Inference at * 1 1 
Iof proof for Lemma dcdr-to-bool-equivalence:



1. P : 
2. d : P  (P)
3. [d]
  P 

latex

 by D 2 

latex

 1: 

 1: 2. x : P
 1: 3. [inl x ]
 1:   P
 2: 

 2: 2. y : P
 2: 3. [inr y ]
 2:   P
 .

Definitions

P  Q, left + right